%===============================================================
%
%     GENERAZIONE DI ESEMPI.   M.O. 08
%
%===============================================================

:- module(genera, [gen/1,
		   is_type/1,
		   is_fun/1,
		   is_pred/1,
		   is_of/2,
		   is_term/3,
		   g_term/3,
		   is_atomic/1,
		   g_atomic/2,
		   is_clause/3,
		   print_clause/1,
		   is_warning/2,
		   in_HU/2,
		   set_max_depth/1
		  ]).

:- consult(gen_msg).
:- use_module(basic_constructs, [predefined_op/5, predefined_atom/3, decompose_body/2]).
:- use_module(utils,[unifies_term/4, normalize_vars/3]).

gen(X) :-
	consult(X).

:- dynamic(max_depth/1).
:- assert(max_depth(1000)).
:- dynamic(tried/0).


set_max_depth(X) :-
	integer(X),
	X > 0,
	retractall(max_depth(_)),
	assert(max_depth(X)).

try(A) :-
	catch(A,E,warn(E)).

warn(E) :-
	not(var(E)),
	(   tried ->
	        fail
	        ;
	        assert(tried),
	        writeln('HAI ESEGUITO LOAD?'),
	        fail
	).

%************************* a type
%

is_type(T) :- try(r__type(T)).

% *************************   a_funct
% SPEC:  a_funct(var X, ?N:int, ?Types:list(a_type), ?T:a_type)
%	 per ogni  f: t1 x ... x tn -> t dichiarata restituisce:
%	 X = f(V1,..,Vn) con variabili fresche V1,..,Vn
%	 N = n
%	 Types = [t1,..,tn],
%	 T = t
%	 ---> EXCEPTION se X non e' una variabile in chiamata

a_funct(X,N,Types,T) :-
	var(X),
	try(r__fun(F,Types,T)),
	length(Types,N),
	length(Args,N),
	X =.. [F|Args].
a_funct(X,_,_,_) :-
	not(var(X)),
	throw(a_funct_error(X, deveEssereUnaVariabile)).

is_fun(F:A->T):- try(r__fun(F,A,T)).

%%  **************************  a_pred
% SPEC:   a_pred(X:var,?N:int, ?Types)  :   restituisce
%           X = p(_X1,..,_Xn), N=n, Types = [t1,..,tn]
%	    per ogni predicato p(t1,..,tn) dichiarato

a_pred(X,N,Types) :-
	var(X),
	try(r__pred(P,Types)),
	length(Types,N),
	length(Args,N),
	X =.. [P|Args].
a_pred(X,_,_) :-
	not(var(X)),
	throw(a_pred_error(X, deveEssereUnaVariabile)).

is_pred(P:A->(o)):- try(r__pred(P,A)).


%******************************************************************
%********************************************   TERMINI  **********

%% ****************************  is_of
%  SPEC:  @X:term is_of -T:a_type :   T e' il tipo di X

is_of(X,_) :-
	var(X),!.
is_of(X,T) :-
	a_funct(F,_N,Types,T),
	unifies_term(X,F,_,Args),
	areOf(Args,Types).
areOf([],[]).
areOf([X|L],[Y|M]) :-
	is_of(X,Y),
	areOf(L,M).


%% *******************************  is_term
%% SPEC:    is_term(?X:term, +T_a_type,+N:int) : X e' un termine di tipo T
%%                                        di profondita' al piu' N
is_term(T,Type,N) :-
	between(0,N,I),
	vt(T,Type,I).

vt(var(_),_T,0).
vt(C,T,0) :-
	a_funct(C,0,_,T).
vt(C,T,N) :-
	N > 0,
	a_funct(F,_N,Types,T),
        unifies_term(C,F,_,Args),
	K is N-1,
	vts(Args,Types,K).

vts([],[],_).
vts([T|A],[TT|TA],K) :-
	is_term(T,TT,K),
	vts(A,TA,K).

%% *******************************  h_elem
%% SPEC: h_elem(?X:term, +T_a_type) : X e' un termine ground di
%% tipo T di profondita' al piu' maxdepth
%%


in_HU(X,T) :-
	max_depth(Max),!,
	between(0,Max,I),
	tt(X,T,I).

%% *******************************  g_term
%% SPEC:    g_term(?X:term, +T_a_type,+N:int) : X e' un termine ground di
%                                         tipo T di profondita' al piu' N
%%

g_term(X,T,K) :-
	between(0,K,I),
	tt(X,T,I).

tt(X,T,0) :-
	a_funct(X,0,_,T).
tt(X,T,H) :-
	H > 0,
	a_funct(F,N,Types,T),
	N > 0,
	unifies_term(X,F,_,Args),
	K is H-1,
	tts(Args,Types,K).

tts([T],[TY],K) :-
	tt(T,TY,K).
tts([T|A],[TT|TA],K) :-
	tt(T,TT,K),
	tts(A,TA,K).


% ********************************************************************************************************
%********************************FORMULE ATOMICHE ******************

%% *************************** an_atomic
%% SPEC:   an_atomic(+A) :  A e' un'atomica ben tipato

is_atomic(A) :-
    a_pred(P,_N,Types),
    unifies_term(A,P,_,Args),
    areOf(Args,Types).

%% ***************************  g_atomic
%%	   g_atomic(?A,+H:int) :  A e' un'atomica ground ben tipato
%%	                        con termini di profondita'
%%	                        massima H

g_atomic(A,H) :-
    a_pred(P,_N,Types),
    unifies_term(A,P,_,Args),
    gts(Args,Types,H).

gts([],[],_).
gts([T|A],[TT|TA],K) :-
	g_term(T,TT,K),
	gts(A,TA,K).


%%	****************************************************** CLAUSOLE
%       usiamo la meta-programmazione per ottenere le clausole del programma corrente

%********************************  is_clause
% SPEC:  is_clause(?P:an_atomic, ?Body:a_body):
%        P e' dichiarato e P :- Body appartiene al programma corrente

is_clause(Context, Head, Body):-
	r__cl(CL),
	(   not(CL = (Head :- Body)) ->
	           Head = CL,
	           Body = true
	           ;
		   CL = (Head :- Body)
	),
	get_context_clause(Head,Body,Cont),
	gr(Cont,Cont),
	normalize_vars('_T', Cont,TypeVars),
	add_type_vars(Cont,Context,TypeVars).

print_clause(_H) :-
	writeln('TO BE IMPLEMENTED').


gr([],[]) :- !.
gr([X|L],[X|L]) :- !, gr(L,L).

add_type_vars(C,C,[]).
add_type_vars(C,[V:type|NC],[V|W]) :-
	add_type_vars(C,NC,W).

% WARNINGS

is_warning(A,B) :-
	r__warning(A,B).


% td, fd, pd ---------------------------------------------------------
%
td(T) :-
	r__type(T).
fd(F,fun(ArgTypes,Type)) :-
	r__fun(F,ArgTypes,Type).
pd(P,pred(ArgTypes)) :-
	r__pred(P,ArgTypes).


% 1. Variable --------------------------------------------------------
get_context_term(X,Type,Context) :-
	is_var(X),
	ins(X:Type,Context).



% 2.  Term, predefined --------------------------------------------
get_context_term(PT,Type,Context) :-
	not(is_var(PT)),
	predefined_op(PT, _F, Args, ArgTypes, Type),
	get_context_list(Args,ArgTypes,Context).


% 2. Term, user defined ----------------------------------------------
get_context_term(T,Type,Context) :-
	not(predefined_op(T,_,_,_,_)),
	T =.. [F|Args],
	fd(F,Ftype),
	copy_term(Ftype,fun(ArgTypes,Type)), % computed types
		% can be different instances
		% of the declared type => POLYMORPHISM
	get_context_list(Args,ArgTypes,Context).

% List of terms
get_context_list([],_,_).

get_context_list([H|L],[TH|TL],Context) :-
	get_context_term(H,TH,Context),
	get_context_list(L,TL,Context).

% 3. Atom (body, predefined)
get_context_atom(A, Context) :-
	predefined_atom(A,Args,Types),
	get_context_list(Args,Types,Context).

% 3. Atom (body)
%
get_context_atom(A, Context) :-
	A =.. [P|Args],
	pd(P,pred(ArgTypes)),
	get_context_list(Args,ArgTypes,Context).

% 4. Formula   --------------------------------------------------------

get_context_fm(F, Context) :-
	decompose_body(F,DF), !,
	get_context_fms(DF, Context).

get_context_fm(F, Context) :-
	get_context_atom(F, Context).

get_context_fms([], _Context).
get_context_fms([F | LF], Context) :-
	get_context_fm(F,Context),
	get_context_fms(LF,Context).


% 5. Clause ------------------------------------------------------------
%
get_context_clause(Head,Body,Context) :-
	get_context_atom(Head,Context),
	get_context_fm(Body, Context).


% ----------------------------------------------------------------------
% individual variables are of the form 'Xn', where n is an integer index

is_var(X) :-
	atom(X),
	atom_concat('X_',I,X),
	is_index(I,_).

is_index(A,N) :-
	atom_to_chars(A,CA),
	to_int(CA,0,N).

to_int([C],N,M) :-
	digit(C,NC),
	M is 10*N + NC.

to_int([C|CL],N,M) :-
	digit(C,NC),
	N1 is 10*N+NC,!,
	to_int(CL,N1,M).

digit(C,N) :-
	N is C-48,
	0 =< N,
	N =< 9.


ins(X,[Y|L]) :- X=Y,!; ins(X,L).












